16 BAIRE'S THEOREM AND ITS CONSEQUENCES 85 neighborhood V of 0 in E, and a real number c> 0 such that p(x) g c for all x e x0 + V. Hence p(z) £X*o) + P(XO + z)£c+ p(x0) for all zeV, which proves the result (12.14.2). (12.16.4) (Banach-Steinhaus theorem) Let E be a Frechet space, F a normed space. Let Hbea set of continuous linear mappings ofE into F. Suppose that sup \\u(x)\\ < + oo for alt x e E. Then H is equicontinuous. UGH The function p(x) = sup ||t/(.x)||, being finite for all x € E, is a seminorm ueH on E (12.14.1). Since each of the functions jci-»||w(jt)|| is continuous, p is lower semicontinuous (12.7.7). The result therefore follows from (12.16.3) and (12.15.7.1). As a consequence, we have: (12.16.5) (i) Under the hypotheses of (12.16.4), let (un) be a sequence of continuous linear mappings ofE into F which converges simply in Etoa mapping uofE into F. Then u is a continuous linear mapping ofE into F. (ii) More generally, let Z be a metric space, A a subset ofZ, and z\~*uza mapping of A into the space of continuous linear mappings of E into F. Let z0 e Z be a point in the closure of A, and suppose that the limit lim uz(x) = v(x) Z-+ZQ, ze A exists in F, for each xeE. Then v is a continuous linear mapping ofE into F. (i) From the hypotheses we have sup ||z/n(x)|| < +00 for all x e E, hence n the Banach-Steinhaus theorem shows that the sequence («„) is equicontinuous, and the continuity of u follows from (7.5.5). The fact that u is linear is an immediate consequence of the principle of extension of identities. (ii) The point z0 is the limit of a sequence of points (zn) in A (3.13.13), hence v(x) == lim uZn(x) for all x e E. Now apply (i). n-* oo (12.16.6) Let E be a Fr&chet space, F a Banach space, I an open interval in R. Let £?(E; F) denote the space of continuous linear mappings ofE into F, endowed with the topology of simple convergence (12.15). If a mapping *h-+/f of I into £?(E; F) is differentiable with respect to the topology of simple convergence (12.15), then there exists a mapping fi-+/J of I into &(E; F) such that = D(ft(x))forallxeE.point x0 e E, ace or a locally compact metrizable space (by virtue